\begin{tabbing}
st{-}key{-}match(${\it tab}$;$k_{1}$;$k_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $k_{1}$\+
\\[0ex]o\=f inl($n$) =$>$ \=case $k_{2}$\+\+
\\[0ex]o\=f inl($m$) =$>$ ff\+
\\[0ex]$\mid$ inr($a$) =$>$ \=($n$ $<$z ptr(${\it tab}$) $\wedge_{b}$ $n$ $<$z $\parallel$${\it tab}$$\parallel$ )\+
\\[0ex]$\wedge_{b}$ eq\_atom1(st{-}atom(${\it tab}$;$n$);$a$)
\-\-\-\\[0ex]$\mid$ inr($a$) =$>$ \=case $k_{2}$\+
\\[0ex]o\=f inl($n$) =$>$ \=($n$ $<$z ptr(${\it tab}$) $\wedge_{b}$ $n$ $<$z $\parallel$${\it tab}$$\parallel$ )\+\+
\\[0ex]$\wedge_{b}$ eq\_atom1(st{-}atom(${\it tab}$;$n$);$a$)
\-\\[0ex]$\mid$ inr($b$) =$>$ ff
\-\-\-\-
\end{tabbing}